Implement inheritance condition for Mutable types #24253
Conversation
| - `{x, ...}.RD = {x.rd, ...}.RD` | ||
| - `{x.rd, ...} <: {x, ...}` | ||
|
|
||
| ## Separation Checking |
There was a problem hiding this comment.
Why are we dropping all these descriptions on separation checking?
There was a problem hiding this comment.
They are in a separate file: separation-checking.md
| **Restriction:** A non-mutable type cannot be downcast by a pattern match to a mutable type. (Note: This is currently not enforced) | ||
|
|
||
| **Definition:** A class is _read_only_ if the following conditions are met: | ||
| **Definition:** A parent class constructor is _read-only_ if the following conditions are met: |
There was a problem hiding this comment.
I'm trying to make sense of this restriction: does it mean that if you decide to mark a class as mutation-tracked, then all exclusive capability from this class must also be tracked?
There was a problem hiding this comment.
Yes, exactly. Because when we widen the type to something that does not extend Mutable, we make the capture set read-only.
| When we create an instance of a mutable type we always add `cap` to its capture set. For instance, if class `Ref` is declared as shown previously then `new Ref(1)` has type `Ref[Int]^`. | ||
|
|
||
| **Restriction:** A non-mutable type cannot be downcast by a pattern match to a mutable type. | ||
| **Restriction:** A non-mutable type cannot be downcast by a pattern match to a mutable type. (Note: This is currently not enforced) |
There was a problem hiding this comment.
I thought a bit about this and was wondering whether we can do this by inspecting capture sets in the pattern: one may never "widen" a readonly set to a exclusive one since that will be a permission upgrade.
So instead of preventing narrowing we prevent widening, very much like what we are already doing for capture sets.
odersky
force-pushed
the
implement-mutable-inheritance
branch
from
f4b401e to
97a2ef2
Compare
4 participants
No description provided.